es:ES, R:(EE).
(e, e':E. Dec(R(e',e)))
 R => x,y. (x < y)
 (e, e':E. Dec(es-r-immediate-pred(es;R;e';e))) 

latex

Definitions	R1 => R2, es-r-immediate-pred(es;R;e';e), R!, ES, , Type, (e < e'), x f y, A, False, P  Q, Dec(P), x:A. B(x), x:AB(x), Void, P & Q, x:A  B(x), f(a), E, x:A. B(x), x. t(x), x.A(x), x:A.B(x), t  T, left + right, P  Q, A c B, t.1, e < e', b
Lemmas	es-causl wf, not wf, decidable existse-causl, decidable and, decidable cand